COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE PREDCONST SEXP 1[R←350]
C00005 ENDMK
C⊗;
DECLARE PREDCONST SEXP 1[R←350];
DECLARE PREDCONST LIST 1[R←350];

DECLARE INDVAR X X0 X1 X2 Y Y0 Y1 Y2 Z Z0 Z1 Z2;
DECLARE INDVAR x x0 x1 x2 y y0 y1 y2 z z0 z1 z2 ε SEXP;
DECLARE INDVAR u u0 u1 u2 v v0 v1 v2 w w0 w1 w2 ε LIST;
DECLARE INDCONST NILL ε LIST;

AXIOM SEXP: ∀x.SEXP x;;
AXIOM LIST: ∀u.LIST u;;

MOREGENERAL SEXP ≥ {LIST};

DECLARE OPCONST CONS 2;
DECLARE OPCONST CAR 1[R ← 600];
DECLARE OPCONST CDR 1[R ← 600];

DECLARE PREDCONST ATOM 1[R ← 500];
DECLARE PREDCONST NULL 1[R ← 500];

AXIOM CONS:
	∀x y.SEXP CONS(x,y)
	∀x u.LIST CONS(x,u)
;;

AXIOM CAR:
	∀x.(¬ATOM x ⊃ SEXP CAR x)
;;

AXIOM CDR:
	∀x.(¬ATOM x ⊃ SEXP CDR x)
	∀u.(¬u=NILL ⊃ LIST CDR u)
;;

AXIOM NILL:
	∀u.(ATOM u ≡ u = NILL)
	∀u.(NULL u ≡ u = NILL)
;;

AXIOM LISP:
	∀x y.¬ATOM CONS(x,y)
	∀x y.(CAR CONS(x,y) = x)
	∀x y.(CDR CONS(x,y) = y)
	∀y.(¬ATOM y ⊃ y = CONS(CAR y,CDR y))
;;

DECLARE PREDCONST IN(SEXP,SEXP)[L←250,R←255];

AXIOM IN:
	∀x.(¬ATOM x ⊃ CAR x IN x)
	∀x.(¬ATOM x ⊃ CDR x IN x)
	∀x y.(x IN CONS(x,y))
	∀x y.(y IN CONS(x,y))
	∀x.¬x IN x
	∀x y z.(x IN y ∧ y IN z ⊃ x IN z)
;;

DECLARE PREDPAR P 1;

AXIOM INDUCTION:
	∀x.(ATOM x ⊃ P(x)) ∧ ∀x.(¬ATOM x ∧ P(CAR x) ∧ P(CDR x) ⊃ P(x)) ⊃ ∀x.P(x)
	P(NILL) ∧ ∀u.(¬(u=NILL) ∧ P(CDR u) ⊃ P(u)) ⊃ ∀u.P(u)
	∀x.(ATOM x ⊃ P(x)) ∧ ∀x.(∀y.(y IN x ⊃ P(y))) ⊃ ∀x.P(x)
;;